Nuprl Definition : ecl-mng-sends 11,40

ecl-mng-sends{i:l}
ecl-mng-sends(es; i; ds; da; x; l; snd)
== es-decls(es;i;ds;da)
==  with decls ds 
==  with decls da
==  sends on l from e 
==  include tagged-list-messages(es-state-when(es; e);
==  include tagged-list-messages(es-val(es; e);
==  include tagged-list-messages(mapfilter((tr.<tr.1, tr.2.2>);
==  include tagged-list-messages(mapfilter((tr.es-bact{i:l}
==  include tagged-list-messages(mapfilter((tr.es-bact(ds;
==  include tagged-list-messages(mapfilter((tr.es-bact(da;
==  include tagged-list-messages(mapfilter((tr.es-bact(x;
==  include tagged-list-messages(mapfilter((tr.es-bact(es;
==  include tagged-list-messages(mapfilter((tr.es-bact(((tr.2).1);
==  include tagged-list-messages(mapfilter((tr.es-bact(es-init(es;e);
==  include tagged-list-messages(mapfilter((tr.es-bact(e));
==  include tagged-list-messages(mapfilter(fpf-cap(snd;
==  include tagged-list-messages(mapfilter(fpf-cap(product-deq(Knd; IdLnk; Kind-deq; idlnk-deq);
==  include tagged-list-messages(mapfilter(fpf-cap(<es-kind(es; e), l>;
==  include tagged-list-messages(mapfilter(fpf-cap([]))) 
==  and only these for tags in ecl-tags(l; snd) 
latex



clarification:

ecl-mng-sends{i:l}
ecl-mng-sends(es; i; ds; da; x; l; snd)
== es-decls(es;i;ds;da)
==  es-sends-iff(es;l;ecl-tags(l; snd);da;ds;e.tagged-list-messages(es-state-when(es; e);
==  es-sends-iff(es;l;ecl-tags(l; snd);da;ds;e.tagged-list-messages(es-val(es; e);
==  es-sends-iff(es;l;ecl-tags(l; snd);da;ds;e.tagged-list-messages(mapfilter
==  es-sends-iff(es;l;ecl-tags(l; snd);da;ds;e.tagged-list-messages(((tr.<tr.1, tr.2.2>);
==  es-sends-iff(es;l;ecl-tags(l; snd);da;ds;e.tagged-list-messages(((tr.es-bact{i:l}
==  es-sends-iff(es;l;ecl-tags(l; snd);da;ds;e.tagged-list-messages(((tr.es-bact(ds;
==  es-sends-iff(es;l;ecl-tags(l; snd);da;ds;e.tagged-list-messages(((tr.es-bact(da;
==  es-sends-iff(es;l;ecl-tags(l; snd);da;ds;e.tagged-list-messages(((tr.es-bact(x;
==  es-sends-iff(es;l;ecl-tags(l; snd);da;ds;e.tagged-list-messages(((tr.es-bact(es;
==  es-sends-iff(es;l;ecl-tags(l; snd);da;ds;e.tagged-list-messages(((tr.es-bact(((tr.2).1);
==  es-sends-iff(es;l;ecl-tags(l; snd);da;ds;e.tagged-list-messages(((tr.es-bact(es-init(es;e);
==  es-sends-iff(es;l;ecl-tags(l; snd);da;ds;e.tagged-list-messages(((tr.es-bact(e));
==  es-sends-iff(es;l;ecl-tags(l; snd);da;ds;e.tagged-list-messages((fpf-cap(snd;
==  es-sends-iff(es;l;ecl-tags(l; snd);da;ds;e.tagged-list-messages((fpf-cap(product-deq(Knd;
==  es-sends-iff(es;l;ecl-tags(l; snd);da;ds;e.tagged-list-messages((fpf-cap(product-deq(IdLnk;
==  es-sends-iff(es;l;ecl-tags(l; snd);da;ds;e.tagged-list-messages((fpf-cap(product-deq(Kind-deq;
==  es-sends-iff(es;l;ecl-tags(l; snd);da;ds;e.tagged-list-messages((fpf-cap(product-deq(idlnk-deq
==  es-sends-iff(es;l;ecl-tags(l; snd);da;ds;e.tagged-list-messages((fpf-cap(product-deq();
==  es-sends-iff(es;l;ecl-tags(l; snd);da;ds;e.tagged-list-messages((fpf-cap(<es-kind(es; e), l>;
==  es-sends-iff(es;l;ecl-tags(l; snd);da;ds;e.tagged-list-messages((fpf-cap([])))) 
latex


Definitions[], es-kind(es; e), <a, b>, idlnk-deq, Kind-deq, IdLnk, Knd, product-deq(A; B; a; b), fpf-cap(f; eq; x; z), es-init(es;e), t.2, t.1, es-bact{i:l}(ds; da; a; es; n; e1; e2), x.A(x), mapfilter(f; P; L), es-val(es; e), es-state-when(es; e), tagged-list-messages(s; v; L), ecl-tags(l; snd), with decls ds dasends on l from e include f(e) and only these for tags in tgs, es-decls(es;i;ds;da), P  Q
FDL editor aliasesecl-mng-sends

origin